Inference at * 1 
Iof proof for Lemma can-apply-fun-exp:



1. A : Type
2. f : A(A + Top)
3. n : 
4. 0 < n
5. y:A. (isl(f^n - 1(y)))  (m:. (m  (n - 1))  (isl(f^m(y))))
6. y : A
7. m : 
8. m  n
9. (m = 0)
  (isl(f^n - 1 o f^1  (y)))  (isl(f^m - 1 o f^1  (y))) 

latex

 by (RepUR ``p-compose can-apply do-apply`` ( 0)) 
CollapseTHEN (((GenConclAtAddr [1;1;1;1;1]) 

CoCollapseTHENA (Auto)) 
CollapseTHEN ((D (-2)) 
CollapseTHEN ((Reduce 0) 
CollapseTHEN ((
CAuto) 
CollapseTHEN (((if ((0) = 0) then BackThruSomeHyp else BHyp (0) )) 
CollapseTHEN (Auto
C)))))) 

latex

C.

Definitions	f o g  , can-apply(f;x), do-apply(f;x), s = t, left + right, isl(x), Top, f(a), f^n, , {x:A| B(x)} , , #$n, A  B, A, x:AB(x), Void, a < b, n - m, n+m, -n, b, P  Q, x:A. B(x), t  T, False
Lemmas	assert wf, isl wf, p-fun-exp wf, le wf, false wf